definitionally equal
from Theorem Proving in Lean 4
原則として、同じ値に簡約される2つの項はdefinitionally equalであると呼ばれる。Leanの型チェッカーはdefinitionally equalである2つの項を「同じ」とみなす。Leanは2つの項の間の相等関係を認識しサポートするために最善を尽くす。ref
実際、Leanのカーネルは (fun x => t) s と t[s/x](項 t の中の全ての x を s で置き換えた項) をdefinitionally equalとみなすのと同様に、任意の p : Prop に対して任意の2つの項 t1 t2 : p をdefinitionally equalとみなす。t1 t2 : p をdefinitionally equalとみなすことはproof irrelevance(証明無関係)と呼ばれ、前段落の解釈と矛盾しない。つまり、証明 t : p は依存型理論の言語の中で普通の項として扱うことができるが、t は p が真であるという事実以上の情報は持っていないということである。ref